Nuprl Definition : fpf-val
0,22
postcript
pdf
z
!=
f
(
x
)
P
(
a
;
z
) ==
x
dom(
f
)
P
(
x
;
f
(
x
))
latex
clarification:
fpf-val(
eq
;
f
;
x
;
a
,
z
.
P
(
a
;
z
)) == fpf-dom(
eq
;
x
;
f
)
P
(
x
;fpf-ap(
f
;
eq
;
x
))
latex
Definitions
f
(
x
)
,
x
dom(
f
)
,
b
,
P
Q
FDL editor aliases
fpf-val
origin
P(a;z) == x 
dom(f) P(x;f(x))
P(x;fpf-ap(f; eq; x)) P(a;z) == x dom(f) P(x;f(x))
P(x;fpf-ap(f; eq; x)) dom(f)
b Q